H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 4.003 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Lambda Reductions:
The following Lambda expression

\vu68→

case vu68 of
(cs@(_ : _),t) → (cs,t) : []

_ → []

is transformed to

nonnull0 vu68 =

case vu68 of
(cs@(_ : _),t) → (cs,t) : []

_ → []

The following Lambda expression

\(_,zs)→zs

is transformed to

zs0 (_,zs) = zs

The following Lambda expression

\(ys,_)→ys

is transformed to

ys0 (ys,_) = ys

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Case Reductions:
The following Case expression

case vu68 of
(cs@(_ : _),t) → (cs,t) : []

_ → []

is transformed to

nonnull00 (cs@(_ : _),t) = (cs,t) : []

nonnull00 _ = []

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern

cs@(vy : vz)

is replaced by the following term

vy : vz

The bind variable of the following binding Pattern

xs@(wv : ww)

is replaced by the following term

wv : ww

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

span p [] = ([],[])

span p (wv : ww)

| p wv

= (wv : ys,zs)

| otherwise

= ([],wv : ww)

where

vu43 = span p ww

ys = ys0 vu43

ys0 (ys,wx) = ys

zs = zs0 vu43

zs0 (wy,zs) = zs

is transformed to

span p [] = span3 p []

span p (wv : ww) = span2 p (wv : ww)

span2 p (wv : ww) =

span1 p wv ww (p wv)

where

span0 p wv ww True = ([],wv : ww)

span1 p wv ww True = (wv : ys,zs)

span1 p wv ww False = span0 p wv ww otherwise

vu43 = span p ww

ys = ys0 vu43

ys0 (ys,wx) = ys

zs = zs0 vu43

zs0 (wy,zs) = zs

span3 p [] = ([],[])

span3 xw xx = span2 xw xx

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

span1 p wv ww (p wv)

where

span0 p wv ww True = ([],wv : ww)

span1 p wv ww True = (wv : ys,zs)

span1 p wv ww False = span0 p wv ww otherwise

vu43 = span p ww

ys = ys0 vu43

ys0 (ys,wx) = ys

zs = zs0 vu43

zs0 (wy,zs) = zs

are unpacked to the following functions on top level

span2Ys0 xy xz (ys,wx) = ys

span2Zs0 xy xz (wy,zs) = zs

span2Ys xy xz = span2Ys0 xy xz (span2Vu43 xy xz)

span2Vu43 xy xz = span xy xz

span2Span1 xy xz p wv ww True = (wv : span2Ys xy xz,span2Zs xy xz)

span2Span1 xy xz p wv ww False = span2Span0 xy xz p wv ww otherwise

span2Zs xy xz = span2Zs0 xy xz (span2Vu43 xy xz)

span2Span0 xy xz p wv ww True = ([],wv : ww)

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

mainModule Main

((lexDigits :: [Char] -> [([Char],[Char])]) :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

mainModule Main

(lexDigits :: [Char] -> [([Char],[Char])])

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="lexDigits",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="lexDigits yu3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="nonnull isDigit yu3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="concatMap nonnull0 (span isDigit yu3 : [])",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="concat . map nonnull0",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="concat (map nonnull0 (span isDigit yu3 : []))",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="foldr (++) [] (map nonnull0 (span isDigit yu3 : []))",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="foldr (++) [] (nonnull0 (span isDigit yu3) : map nonnull0 [])",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="(++) nonnull0 (span isDigit yu3) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="(++) nonnull00 (span isDigit yu3) foldr (++) [] (map nonnull0 [])",fontsize=16,color="burlywood",shape="box"];1783[label="yu3/yu30 : yu31",fontsize=10,color="white",style="solid",shape="box"];11 -> 1783[label="",style="solid", color="burlywood", weight=9];
1783 -> 12[label="",style="solid", color="burlywood", weight=3];
1784[label="yu3/[]",fontsize=10,color="white",style="solid",shape="box"];11 -> 1784[label="",style="solid", color="burlywood", weight=9];
1784 -> 13[label="",style="solid", color="burlywood", weight=3];
12[label="(++) nonnull00 (span isDigit (yu30 : yu31)) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="(++) nonnull00 (span isDigit []) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];13 -> 15[label="",style="solid", color="black", weight=3];
14[label="(++) nonnull00 (span2 isDigit (yu30 : yu31)) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15[label="(++) nonnull00 (span3 isDigit []) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="(++) nonnull00 (span2Span1 isDigit yu31 isDigit yu30 yu31 (isDigit yu30)) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="(++) nonnull00 ([],[]) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];17 -> 19[label="",style="solid", color="black", weight=3];
18 -> 25[label="",style="dashed", color="red", weight=0];
18[label="(++) nonnull00 (span2Span1 isDigit yu31 isDigit yu30 yu31 (yu30 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))) && yu30 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) foldr (++) [] (map nonnull0 [])",fontsize=16,color="magenta"];18 -> 26[label="",style="dashed", color="magenta", weight=3];
18 -> 27[label="",style="dashed", color="magenta", weight=3];
18 -> 28[label="",style="dashed", color="magenta", weight=3];
18 -> 29[label="",style="dashed", color="magenta", weight=3];
19[label="(++) [] foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="box"];19 -> 24[label="",style="solid", color="black", weight=3];
26[label="yu31",fontsize=16,color="green",shape="box"];27[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];28[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];29[label="yu30",fontsize=16,color="green",shape="box"];25[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (yu10 >= Char (Succ yu11) && yu10 <= Char (Succ yu12))) foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="triangle"];25 -> 34[label="",style="solid", color="black", weight=3];
24[label="foldr (++) [] (map nonnull0 [])",fontsize=16,color="black",shape="triangle"];24 -> 35[label="",style="solid", color="black", weight=3];
34 -> 36[label="",style="dashed", color="red", weight=0];
34[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (compare yu10 (Char (Succ yu11)) /= LT && yu10 <= Char (Succ yu12))) foldr (++) [] (map nonnull0 [])",fontsize=16,color="magenta"];34 -> 37[label="",style="dashed", color="magenta", weight=3];
35[label="foldr (++) [] []",fontsize=16,color="black",shape="box"];35 -> 38[label="",style="solid", color="black", weight=3];
37 -> 24[label="",style="dashed", color="red", weight=0];
37[label="foldr (++) [] (map nonnull0 [])",fontsize=16,color="magenta"];36[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (compare yu10 (Char (Succ yu11)) /= LT && yu10 <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="triangle"];36 -> 39[label="",style="solid", color="black", weight=3];
38[label="[]",fontsize=16,color="green",shape="box"];39[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (not (compare yu10 (Char (Succ yu11)) == LT) && yu10 <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="box"];39 -> 40[label="",style="solid", color="black", weight=3];
40[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit yu10 yu9 (not (primCmpChar yu10 (Char (Succ yu11)) == LT) && yu10 <= Char (Succ yu12))) yu13",fontsize=16,color="burlywood",shape="box"];1788[label="yu10/Char yu100",fontsize=10,color="white",style="solid",shape="box"];40 -> 1788[label="",style="solid", color="burlywood", weight=9];
1788 -> 41[label="",style="solid", color="burlywood", weight=3];
41[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char yu100) yu9 (not (primCmpChar (Char yu100) (Char (Succ yu11)) == LT) && Char yu100 <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="box"];41 -> 42[label="",style="solid", color="black", weight=3];
42[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char yu100) yu9 (not (primCmpNat yu100 (Succ yu11) == LT) && Char yu100 <= Char (Succ yu12))) yu13",fontsize=16,color="burlywood",shape="box"];1789[label="yu100/Succ yu1000",fontsize=10,color="white",style="solid",shape="box"];42 -> 1789[label="",style="solid", color="burlywood", weight=9];
1789 -> 43[label="",style="solid", color="burlywood", weight=3];
1790[label="yu100/Zero",fontsize=10,color="white",style="solid",shape="box"];42 -> 1790[label="",style="solid", color="burlywood", weight=9];
1790 -> 44[label="",style="solid", color="burlywood", weight=3];
43[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Succ yu1000)) yu9 (not (primCmpNat (Succ yu1000) (Succ yu11) == LT) && Char (Succ yu1000) <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="box"];43 -> 45[label="",style="solid", color="black", weight=3];
44[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char Zero) yu9 (not (primCmpNat Zero (Succ yu11) == LT) && Char Zero <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="box"];44 -> 46[label="",style="solid", color="black", weight=3];
45 -> 344[label="",style="dashed", color="red", weight=0];
45[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char (Succ yu1000)) yu9 (not (primCmpNat yu1000 yu11 == LT) && Char (Succ yu1000) <= Char (Succ yu12))) yu13",fontsize=16,color="magenta"];45 -> 345[label="",style="dashed", color="magenta", weight=3];
45 -> 346[label="",style="dashed", color="magenta", weight=3];
45 -> 347[label="",style="dashed", color="magenta", weight=3];
45 -> 348[label="",style="dashed", color="magenta", weight=3];
45 -> 349[label="",style="dashed", color="magenta", weight=3];
45 -> 350[label="",style="dashed", color="magenta", weight=3];
46[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char Zero) yu9 (not (LT == LT) && Char Zero <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="box"];46 -> 49[label="",style="solid", color="black", weight=3];
345[label="yu1000",fontsize=16,color="green",shape="box"];346[label="yu9",fontsize=16,color="green",shape="box"];347[label="yu11",fontsize=16,color="green",shape="box"];348[label="yu12",fontsize=16,color="green",shape="box"];349[label="yu13",fontsize=16,color="green",shape="box"];350[label="yu1000",fontsize=16,color="green",shape="box"];344[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat yu29 yu30 == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="burlywood",shape="triangle"];1792[label="yu29/Succ yu290",fontsize=10,color="white",style="solid",shape="box"];344 -> 1792[label="",style="solid", color="burlywood", weight=9];
1792 -> 399[label="",style="solid", color="burlywood", weight=3];
1793[label="yu29/Zero",fontsize=10,color="white",style="solid",shape="box"];344 -> 1793[label="",style="solid", color="burlywood", weight=9];
1793 -> 400[label="",style="solid", color="burlywood", weight=3];
49[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char Zero) yu9 (not True && Char Zero <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="box"];49 -> 54[label="",style="solid", color="black", weight=3];
399[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat (Succ yu290) yu30 == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="burlywood",shape="box"];1794[label="yu30/Succ yu300",fontsize=10,color="white",style="solid",shape="box"];399 -> 1794[label="",style="solid", color="burlywood", weight=9];
1794 -> 401[label="",style="solid", color="burlywood", weight=3];
1795[label="yu30/Zero",fontsize=10,color="white",style="solid",shape="box"];399 -> 1795[label="",style="solid", color="burlywood", weight=9];
1795 -> 402[label="",style="solid", color="burlywood", weight=3];
400[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat Zero yu30 == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="burlywood",shape="box"];1796[label="yu30/Succ yu300",fontsize=10,color="white",style="solid",shape="box"];400 -> 1796[label="",style="solid", color="burlywood", weight=9];
1796 -> 403[label="",style="solid", color="burlywood", weight=3];
1797[label="yu30/Zero",fontsize=10,color="white",style="solid",shape="box"];400 -> 1797[label="",style="solid", color="burlywood", weight=9];
1797 -> 404[label="",style="solid", color="burlywood", weight=3];
54[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char Zero) yu9 (False && Char Zero <= Char (Succ yu12))) yu13",fontsize=16,color="black",shape="box"];54 -> 59[label="",style="solid", color="black", weight=3];
401[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat (Succ yu290) (Succ yu300) == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];401 -> 405[label="",style="solid", color="black", weight=3];
402[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat (Succ yu290) Zero == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];402 -> 406[label="",style="solid", color="black", weight=3];
403[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat Zero (Succ yu300) == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];403 -> 407[label="",style="solid", color="black", weight=3];
404[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat Zero Zero == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];404 -> 408[label="",style="solid", color="black", weight=3];
59[label="(++) nonnull00 (span2Span1 isDigit yu9 isDigit (Char Zero) yu9 False) yu13",fontsize=16,color="black",shape="box"];59 -> 65[label="",style="solid", color="black", weight=3];
405 -> 344[label="",style="dashed", color="red", weight=0];
405[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat yu290 yu300 == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="magenta"];405 -> 409[label="",style="dashed", color="magenta", weight=3];
405 -> 410[label="",style="dashed", color="magenta", weight=3];
406[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (GT == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];406 -> 411[label="",style="solid", color="black", weight=3];
407[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (LT == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];407 -> 412[label="",style="solid", color="black", weight=3];
408[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (EQ == LT) && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];408 -> 413[label="",style="solid", color="black", weight=3];
65[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char Zero) yu9 otherwise) yu13",fontsize=16,color="black",shape="box"];65 -> 73[label="",style="solid", color="black", weight=3];
409[label="yu300",fontsize=16,color="green",shape="box"];410[label="yu290",fontsize=16,color="green",shape="box"];411[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not False && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="triangle"];411 -> 414[label="",style="solid", color="black", weight=3];
412[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not True && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];412 -> 415[label="",style="solid", color="black", weight=3];
413 -> 411[label="",style="dashed", color="red", weight=0];
413[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not False && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="magenta"];73[label="(++) nonnull00 (span2Span0 isDigit yu9 isDigit (Char Zero) yu9 True) yu13",fontsize=16,color="black",shape="box"];73 -> 81[label="",style="solid", color="black", weight=3];
414[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (True && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];414 -> 416[label="",style="solid", color="black", weight=3];
415[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (False && Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];415 -> 417[label="",style="solid", color="black", weight=3];
81[label="(++) nonnull00 ([],Char Zero : yu9) yu13",fontsize=16,color="black",shape="box"];81 -> 90[label="",style="solid", color="black", weight=3];
416[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (Char (Succ yu28) <= Char (Succ yu31))) yu32",fontsize=16,color="black",shape="box"];416 -> 418[label="",style="solid", color="black", weight=3];
417[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 False) yu32",fontsize=16,color="black",shape="triangle"];417 -> 419[label="",style="solid", color="black", weight=3];
90[label="(++) [] yu13",fontsize=16,color="black",shape="triangle"];90 -> 100[label="",style="solid", color="black", weight=3];
418[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (compare (Char (Succ yu28)) (Char (Succ yu31)) /= GT)) yu32",fontsize=16,color="black",shape="box"];418 -> 420[label="",style="solid", color="black", weight=3];
419[label="(++) nonnull00 (span2Span0 isDigit yu27 isDigit (Char (Succ yu28)) yu27 otherwise) yu32",fontsize=16,color="black",shape="box"];419 -> 421[label="",style="solid", color="black", weight=3];
100[label="yu13",fontsize=16,color="green",shape="box"];420[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (compare (Char (Succ yu28)) (Char (Succ yu31)) == GT))) yu32",fontsize=16,color="black",shape="box"];420 -> 422[label="",style="solid", color="black", weight=3];
421[label="(++) nonnull00 (span2Span0 isDigit yu27 isDigit (Char (Succ yu28)) yu27 True) yu32",fontsize=16,color="black",shape="box"];421 -> 423[label="",style="solid", color="black", weight=3];
422[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpChar (Char (Succ yu28)) (Char (Succ yu31)) == GT))) yu32",fontsize=16,color="black",shape="box"];422 -> 424[label="",style="solid", color="black", weight=3];
423[label="(++) nonnull00 ([],Char (Succ yu28) : yu27) yu32",fontsize=16,color="black",shape="box"];423 -> 425[label="",style="solid", color="black", weight=3];
424 -> 654[label="",style="dashed", color="red", weight=0];
424[label="(++) nonnull00 (span2Span1 isDigit yu27 isDigit (Char (Succ yu28)) yu27 (not (primCmpNat (Succ yu28) (Succ yu31) == GT))) yu32",fontsize=16,color="magenta"];424 -> 655[label="",style="dashed", color="magenta", weight=3];
424 -> 656[label="",style="dashed", color="magenta", weight=3];
424 -> 657[label="",style="dashed", color="magenta", weight=3];
424 -> 658[label="",style="dashed", color="magenta", weight=3];
424 -> 659[label="",style="dashed", color="magenta", weight=3];
425 -> 90[label="",style="dashed", color="red", weight=0];
425[label="(++) [] yu32",fontsize=16,color="magenta"];425 -> 427[label="",style="dashed", color="magenta", weight=3];
655[label="Succ yu28",fontsize=16,color="green",shape="box"];656[label="yu32",fontsize=16,color="green",shape="box"];657[label="yu28",fontsize=16,color="green",shape="box"];658[label="yu27",fontsize=16,color="green",shape="box"];659[label="Succ yu31",fontsize=16,color="green",shape="box"];654[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat yu64 yu65 == GT))) yu66",fontsize=16,color="burlywood",shape="triangle"];1802[label="yu64/Succ yu640",fontsize=10,color="white",style="solid",shape="box"];654 -> 1802[label="",style="solid", color="burlywood", weight=9];
1802 -> 705[label="",style="solid", color="burlywood", weight=3];
1803[label="yu64/Zero",fontsize=10,color="white",style="solid",shape="box"];654 -> 1803[label="",style="solid", color="burlywood", weight=9];
1803 -> 706[label="",style="solid", color="burlywood", weight=3];
427[label="yu32",fontsize=16,color="green",shape="box"];705[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat (Succ yu640) yu65 == GT))) yu66",fontsize=16,color="burlywood",shape="box"];1804[label="yu65/Succ yu650",fontsize=10,color="white",style="solid",shape="box"];705 -> 1804[label="",style="solid", color="burlywood", weight=9];
1804 -> 707[label="",style="solid", color="burlywood", weight=3];
1805[label="yu65/Zero",fontsize=10,color="white",style="solid",shape="box"];705 -> 1805[label="",style="solid", color="burlywood", weight=9];
1805 -> 708[label="",style="solid", color="burlywood", weight=3];
706[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat Zero yu65 == GT))) yu66",fontsize=16,color="burlywood",shape="box"];1806[label="yu65/Succ yu650",fontsize=10,color="white",style="solid",shape="box"];706 -> 1806[label="",style="solid", color="burlywood", weight=9];
1806 -> 709[label="",style="solid", color="burlywood", weight=3];
1807[label="yu65/Zero",fontsize=10,color="white",style="solid",shape="box"];706 -> 1807[label="",style="solid", color="burlywood", weight=9];
1807 -> 710[label="",style="solid", color="burlywood", weight=3];
707[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat (Succ yu640) (Succ yu650) == GT))) yu66",fontsize=16,color="black",shape="box"];707 -> 711[label="",style="solid", color="black", weight=3];
708[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat (Succ yu640) Zero == GT))) yu66",fontsize=16,color="black",shape="box"];708 -> 712[label="",style="solid", color="black", weight=3];
709[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat Zero (Succ yu650) == GT))) yu66",fontsize=16,color="black",shape="box"];709 -> 713[label="",style="solid", color="black", weight=3];
710[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat Zero Zero == GT))) yu66",fontsize=16,color="black",shape="box"];710 -> 714[label="",style="solid", color="black", weight=3];
711 -> 654[label="",style="dashed", color="red", weight=0];
711[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (primCmpNat yu640 yu650 == GT))) yu66",fontsize=16,color="magenta"];711 -> 715[label="",style="dashed", color="magenta", weight=3];
711 -> 716[label="",style="dashed", color="magenta", weight=3];
712[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (GT == GT))) yu66",fontsize=16,color="black",shape="box"];712 -> 717[label="",style="solid", color="black", weight=3];
713[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (LT == GT))) yu66",fontsize=16,color="black",shape="box"];713 -> 718[label="",style="solid", color="black", weight=3];
714[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not (EQ == GT))) yu66",fontsize=16,color="black",shape="box"];714 -> 719[label="",style="solid", color="black", weight=3];
715[label="yu640",fontsize=16,color="green",shape="box"];716[label="yu650",fontsize=16,color="green",shape="box"];717[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not True)) yu66",fontsize=16,color="black",shape="box"];717 -> 720[label="",style="solid", color="black", weight=3];
718[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not False)) yu66",fontsize=16,color="black",shape="triangle"];718 -> 721[label="",style="solid", color="black", weight=3];
719 -> 718[label="",style="dashed", color="red", weight=0];
719[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 (not False)) yu66",fontsize=16,color="magenta"];720 -> 417[label="",style="dashed", color="red", weight=0];
720[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 False) yu66",fontsize=16,color="magenta"];720 -> 722[label="",style="dashed", color="magenta", weight=3];
720 -> 723[label="",style="dashed", color="magenta", weight=3];
720 -> 724[label="",style="dashed", color="magenta", weight=3];
721[label="(++) nonnull00 (span2Span1 isDigit yu62 isDigit (Char (Succ yu63)) yu62 True) yu66",fontsize=16,color="black",shape="box"];721 -> 725[label="",style="solid", color="black", weight=3];
722[label="yu63",fontsize=16,color="green",shape="box"];723[label="yu62",fontsize=16,color="green",shape="box"];724[label="yu66",fontsize=16,color="green",shape="box"];725[label="(++) nonnull00 (Char (Succ yu63) : span2Ys isDigit yu62,span2Zs isDigit yu62) yu66",fontsize=16,color="black",shape="box"];725 -> 726[label="",style="solid", color="black", weight=3];
726[label="(++) ((Char (Succ yu63) : span2Ys isDigit yu62,span2Zs isDigit yu62) : []) yu66",fontsize=16,color="black",shape="box"];726 -> 727[label="",style="solid", color="black", weight=3];
727[label="(Char (Succ yu63) : span2Ys isDigit yu62,span2Zs isDigit yu62) : [] ++ yu66",fontsize=16,color="green",shape="box"];727 -> 728[label="",style="dashed", color="green", weight=3];
727 -> 729[label="",style="dashed", color="green", weight=3];
727 -> 730[label="",style="dashed", color="green", weight=3];
728[label="span2Ys isDigit yu62",fontsize=16,color="black",shape="triangle"];728 -> 731[label="",style="solid", color="black", weight=3];
729[label="span2Zs isDigit yu62",fontsize=16,color="black",shape="triangle"];729 -> 732[label="",style="solid", color="black", weight=3];
730 -> 90[label="",style="dashed", color="red", weight=0];
730[label="[] ++ yu66",fontsize=16,color="magenta"];730 -> 733[label="",style="dashed", color="magenta", weight=3];
731[label="span2Ys0 isDigit yu62 (span2Vu43 isDigit yu62)",fontsize=16,color="black",shape="box"];731 -> 734[label="",style="solid", color="black", weight=3];
732[label="span2Zs0 isDigit yu62 (span2Vu43 isDigit yu62)",fontsize=16,color="black",shape="box"];732 -> 735[label="",style="solid", color="black", weight=3];
733[label="yu66",fontsize=16,color="green",shape="box"];734[label="span2Ys0 isDigit yu62 (span isDigit yu62)",fontsize=16,color="burlywood",shape="box"];1812[label="yu62/yu620 : yu621",fontsize=10,color="white",style="solid",shape="box"];734 -> 1812[label="",style="solid", color="burlywood", weight=9];
1812 -> 736[label="",style="solid", color="burlywood", weight=3];
1813[label="yu62/[]",fontsize=10,color="white",style="solid",shape="box"];734 -> 1813[label="",style="solid", color="burlywood", weight=9];
1813 -> 737[label="",style="solid", color="burlywood", weight=3];
735[label="span2Zs0 isDigit yu62 (span isDigit yu62)",fontsize=16,color="burlywood",shape="box"];1814[label="yu62/yu620 : yu621",fontsize=10,color="white",style="solid",shape="box"];735 -> 1814[label="",style="solid", color="burlywood", weight=9];
1814 -> 738[label="",style="solid", color="burlywood", weight=3];
1815[label="yu62/[]",fontsize=10,color="white",style="solid",shape="box"];735 -> 1815[label="",style="solid", color="burlywood", weight=9];
1815 -> 739[label="",style="solid", color="burlywood", weight=3];
736[label="span2Ys0 isDigit (yu620 : yu621) (span isDigit (yu620 : yu621))",fontsize=16,color="black",shape="box"];736 -> 740[label="",style="solid", color="black", weight=3];
737[label="span2Ys0 isDigit [] (span isDigit [])",fontsize=16,color="black",shape="box"];737 -> 741[label="",style="solid", color="black", weight=3];
738[label="span2Zs0 isDigit (yu620 : yu621) (span isDigit (yu620 : yu621))",fontsize=16,color="black",shape="box"];738 -> 742[label="",style="solid", color="black", weight=3];
739[label="span2Zs0 isDigit [] (span isDigit [])",fontsize=16,color="black",shape="box"];739 -> 743[label="",style="solid", color="black", weight=3];
740[label="span2Ys0 isDigit (yu620 : yu621) (span2 isDigit (yu620 : yu621))",fontsize=16,color="black",shape="box"];740 -> 744[label="",style="solid", color="black", weight=3];
741[label="span2Ys0 isDigit [] (span3 isDigit [])",fontsize=16,color="black",shape="box"];741 -> 745[label="",style="solid", color="black", weight=3];
742[label="span2Zs0 isDigit (yu620 : yu621) (span2 isDigit (yu620 : yu621))",fontsize=16,color="black",shape="box"];742 -> 746[label="",style="solid", color="black", weight=3];
743[label="span2Zs0 isDigit [] (span3 isDigit [])",fontsize=16,color="black",shape="box"];743 -> 747[label="",style="solid", color="black", weight=3];
744[label="span2Ys0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (isDigit yu620))",fontsize=16,color="black",shape="box"];744 -> 748[label="",style="solid", color="black", weight=3];
745[label="span2Ys0 isDigit [] ([],[])",fontsize=16,color="black",shape="box"];745 -> 749[label="",style="solid", color="black", weight=3];
746[label="span2Zs0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (isDigit yu620))",fontsize=16,color="black",shape="box"];746 -> 750[label="",style="solid", color="black", weight=3];
747[label="span2Zs0 isDigit [] ([],[])",fontsize=16,color="black",shape="box"];747 -> 751[label="",style="solid", color="black", weight=3];
748 -> 760[label="",style="dashed", color="red", weight=0];
748[label="span2Ys0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (yu620 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))) && yu620 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];748 -> 761[label="",style="dashed", color="magenta", weight=3];
748 -> 762[label="",style="dashed", color="magenta", weight=3];
748 -> 763[label="",style="dashed", color="magenta", weight=3];
748 -> 764[label="",style="dashed", color="magenta", weight=3];
749[label="[]",fontsize=16,color="green",shape="box"];750 -> 770[label="",style="dashed", color="red", weight=0];
750[label="span2Zs0 isDigit (yu620 : yu621) (span2Span1 isDigit yu621 isDigit yu620 yu621 (yu620 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))) && yu620 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];750 -> 771[label="",style="dashed", color="magenta", weight=3];
750 -> 772[label="",style="dashed", color="magenta", weight=3];
750 -> 773[label="",style="dashed", color="magenta", weight=3];
750 -> 774[label="",style="dashed", color="magenta", weight=3];
751[label="[]",fontsize=16,color="green",shape="box"];761[label="yu620",fontsize=16,color="green",shape="box"];762[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];763[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];764[label="yu621",fontsize=16,color="green",shape="box"];760[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (yu76 >= Char (Succ yu78) && yu76 <= Char (Succ yu79)))",fontsize=16,color="black",shape="triangle"];760 -> 769[label="",style="solid", color="black", weight=3];
771[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];772[label="yu620",fontsize=16,color="green",shape="box"];773[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];774[label="yu621",fontsize=16,color="green",shape="box"];770[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (yu81 >= Char (Succ yu83) && yu81 <= Char (Succ yu84)))",fontsize=16,color="black",shape="triangle"];770 -> 779[label="",style="solid", color="black", weight=3];
769[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (compare yu76 (Char (Succ yu78)) /= LT && yu76 <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];769 -> 780[label="",style="solid", color="black", weight=3];
779[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (compare yu81 (Char (Succ yu83)) /= LT && yu81 <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];779 -> 781[label="",style="solid", color="black", weight=3];
780[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (not (compare yu76 (Char (Succ yu78)) == LT) && yu76 <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];780 -> 782[label="",style="solid", color="black", weight=3];
781[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (not (compare yu81 (Char (Succ yu83)) == LT) && yu81 <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];781 -> 783[label="",style="solid", color="black", weight=3];
782[label="span2Ys0 isDigit (yu76 : yu77) (span2Span1 isDigit yu77 isDigit yu76 yu77 (not (primCmpChar yu76 (Char (Succ yu78)) == LT) && yu76 <= Char (Succ yu79)))",fontsize=16,color="burlywood",shape="box"];1818[label="yu76/Char yu760",fontsize=10,color="white",style="solid",shape="box"];782 -> 1818[label="",style="solid", color="burlywood", weight=9];
1818 -> 784[label="",style="solid", color="burlywood", weight=3];
783[label="span2Zs0 isDigit (yu81 : yu82) (span2Span1 isDigit yu82 isDigit yu81 yu82 (not (primCmpChar yu81 (Char (Succ yu83)) == LT) && yu81 <= Char (Succ yu84)))",fontsize=16,color="burlywood",shape="box"];1819[label="yu81/Char yu810",fontsize=10,color="white",style="solid",shape="box"];783 -> 1819[label="",style="solid", color="burlywood", weight=9];
1819 -> 785[label="",style="solid", color="burlywood", weight=3];
784[label="span2Ys0 isDigit (Char yu760 : yu77) (span2Span1 isDigit yu77 isDigit (Char yu760) yu77 (not (primCmpChar (Char yu760) (Char (Succ yu78)) == LT) && Char yu760 <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];784 -> 786[label="",style="solid", color="black", weight=3];
785[label="span2Zs0 isDigit (Char yu810 : yu82) (span2Span1 isDigit yu82 isDigit (Char yu810) yu82 (not (primCmpChar (Char yu810) (Char (Succ yu83)) == LT) && Char yu810 <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];785 -> 787[label="",style="solid", color="black", weight=3];
786[label="span2Ys0 isDigit (Char yu760 : yu77) (span2Span1 isDigit yu77 isDigit (Char yu760) yu77 (not (primCmpNat yu760 (Succ yu78) == LT) && Char yu760 <= Char (Succ yu79)))",fontsize=16,color="burlywood",shape="box"];1820[label="yu760/Succ yu7600",fontsize=10,color="white",style="solid",shape="box"];786 -> 1820[label="",style="solid", color="burlywood", weight=9];
1820 -> 788[label="",style="solid", color="burlywood", weight=3];
1821[label="yu760/Zero",fontsize=10,color="white",style="solid",shape="box"];786 -> 1821[label="",style="solid", color="burlywood", weight=9];
1821 -> 789[label="",style="solid", color="burlywood", weight=3];
787[label="span2Zs0 isDigit (Char yu810 : yu82) (span2Span1 isDigit yu82 isDigit (Char yu810) yu82 (not (primCmpNat yu810 (Succ yu83) == LT) && Char yu810 <= Char (Succ yu84)))",fontsize=16,color="burlywood",shape="box"];1822[label="yu810/Succ yu8100",fontsize=10,color="white",style="solid",shape="box"];787 -> 1822[label="",style="solid", color="burlywood", weight=9];
1822 -> 790[label="",style="solid", color="burlywood", weight=3];
1823[label="yu810/Zero",fontsize=10,color="white",style="solid",shape="box"];787 -> 1823[label="",style="solid", color="burlywood", weight=9];
1823 -> 791[label="",style="solid", color="burlywood", weight=3];
788[label="span2Ys0 isDigit (Char (Succ yu7600) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Succ yu7600)) yu77 (not (primCmpNat (Succ yu7600) (Succ yu78) == LT) && Char (Succ yu7600) <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];788 -> 792[label="",style="solid", color="black", weight=3];
789[label="span2Ys0 isDigit (Char Zero : yu77) (span2Span1 isDigit yu77 isDigit (Char Zero) yu77 (not (primCmpNat Zero (Succ yu78) == LT) && Char Zero <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];789 -> 793[label="",style="solid", color="black", weight=3];
790[label="span2Zs0 isDigit (Char (Succ yu8100) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Succ yu8100)) yu82 (not (primCmpNat (Succ yu8100) (Succ yu83) == LT) && Char (Succ yu8100) <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];790 -> 794[label="",style="solid", color="black", weight=3];
791[label="span2Zs0 isDigit (Char Zero : yu82) (span2Span1 isDigit yu82 isDigit (Char Zero) yu82 (not (primCmpNat Zero (Succ yu83) == LT) && Char Zero <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];791 -> 795[label="",style="solid", color="black", weight=3];
792 -> 1044[label="",style="dashed", color="red", weight=0];
792[label="span2Ys0 isDigit (Char (Succ yu7600) : yu77) (span2Span1 isDigit yu77 isDigit (Char (Succ yu7600)) yu77 (not (primCmpNat yu7600 yu78 == LT) && Char (Succ yu7600) <= Char (Succ yu79)))",fontsize=16,color="magenta"];792 -> 1045[label="",style="dashed", color="magenta", weight=3];
792 -> 1046[label="",style="dashed", color="magenta", weight=3];
792 -> 1047[label="",style="dashed", color="magenta", weight=3];
792 -> 1048[label="",style="dashed", color="magenta", weight=3];
792 -> 1049[label="",style="dashed", color="magenta", weight=3];
793[label="span2Ys0 isDigit (Char Zero : yu77) (span2Span1 isDigit yu77 isDigit (Char Zero) yu77 (not (LT == LT) && Char Zero <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];793 -> 798[label="",style="solid", color="black", weight=3];
794 -> 1149[label="",style="dashed", color="red", weight=0];
794[label="span2Zs0 isDigit (Char (Succ yu8100) : yu82) (span2Span1 isDigit yu82 isDigit (Char (Succ yu8100)) yu82 (not (primCmpNat yu8100 yu83 == LT) && Char (Succ yu8100) <= Char (Succ yu84)))",fontsize=16,color="magenta"];794 -> 1150[label="",style="dashed", color="magenta", weight=3];
794 -> 1151[label="",style="dashed", color="magenta", weight=3];
794 -> 1152[label="",style="dashed", color="magenta", weight=3];
794 -> 1153[label="",style="dashed", color="magenta", weight=3];
794 -> 1154[label="",style="dashed", color="magenta", weight=3];
795[label="span2Zs0 isDigit (Char Zero : yu82) (span2Span1 isDigit yu82 isDigit (Char Zero) yu82 (not (LT == LT) && Char Zero <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];795 -> 801[label="",style="solid", color="black", weight=3];
1045[label="yu78",fontsize=16,color="green",shape="box"];1046[label="yu77",fontsize=16,color="green",shape="box"];1047[label="yu7600",fontsize=16,color="green",shape="box"];1048[label="yu79",fontsize=16,color="green",shape="box"];1049[label="yu7600",fontsize=16,color="green",shape="box"];1044[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat yu88 yu89 == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="burlywood",shape="triangle"];1826[label="yu88/Succ yu880",fontsize=10,color="white",style="solid",shape="box"];1044 -> 1826[label="",style="solid", color="burlywood", weight=9];
1826 -> 1075[label="",style="solid", color="burlywood", weight=3];
1827[label="yu88/Zero",fontsize=10,color="white",style="solid",shape="box"];1044 -> 1827[label="",style="solid", color="burlywood", weight=9];
1827 -> 1076[label="",style="solid", color="burlywood", weight=3];
798[label="span2Ys0 isDigit (Char Zero : yu77) (span2Span1 isDigit yu77 isDigit (Char Zero) yu77 (not True && Char Zero <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];798 -> 806[label="",style="solid", color="black", weight=3];
1150[label="yu8100",fontsize=16,color="green",shape="box"];1151[label="yu82",fontsize=16,color="green",shape="box"];1152[label="yu83",fontsize=16,color="green",shape="box"];1153[label="yu8100",fontsize=16,color="green",shape="box"];1154[label="yu84",fontsize=16,color="green",shape="box"];1149[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat yu100 yu101 == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="burlywood",shape="triangle"];1828[label="yu100/Succ yu1000",fontsize=10,color="white",style="solid",shape="box"];1149 -> 1828[label="",style="solid", color="burlywood", weight=9];
1828 -> 1185[label="",style="solid", color="burlywood", weight=3];
1829[label="yu100/Zero",fontsize=10,color="white",style="solid",shape="box"];1149 -> 1829[label="",style="solid", color="burlywood", weight=9];
1829 -> 1186[label="",style="solid", color="burlywood", weight=3];
801[label="span2Zs0 isDigit (Char Zero : yu82) (span2Span1 isDigit yu82 isDigit (Char Zero) yu82 (not True && Char Zero <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];801 -> 811[label="",style="solid", color="black", weight=3];
1075[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat (Succ yu880) yu89 == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="burlywood",shape="box"];1830[label="yu89/Succ yu890",fontsize=10,color="white",style="solid",shape="box"];1075 -> 1830[label="",style="solid", color="burlywood", weight=9];
1830 -> 1096[label="",style="solid", color="burlywood", weight=3];
1831[label="yu89/Zero",fontsize=10,color="white",style="solid",shape="box"];1075 -> 1831[label="",style="solid", color="burlywood", weight=9];
1831 -> 1097[label="",style="solid", color="burlywood", weight=3];
1076[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat Zero yu89 == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="burlywood",shape="box"];1832[label="yu89/Succ yu890",fontsize=10,color="white",style="solid",shape="box"];1076 -> 1832[label="",style="solid", color="burlywood", weight=9];
1832 -> 1098[label="",style="solid", color="burlywood", weight=3];
1833[label="yu89/Zero",fontsize=10,color="white",style="solid",shape="box"];1076 -> 1833[label="",style="solid", color="burlywood", weight=9];
1833 -> 1099[label="",style="solid", color="burlywood", weight=3];
806[label="span2Ys0 isDigit (Char Zero : yu77) (span2Span1 isDigit yu77 isDigit (Char Zero) yu77 (False && Char Zero <= Char (Succ yu79)))",fontsize=16,color="black",shape="box"];806 -> 816[label="",style="solid", color="black", weight=3];
1185[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat (Succ yu1000) yu101 == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="burlywood",shape="box"];1834[label="yu101/Succ yu1010",fontsize=10,color="white",style="solid",shape="box"];1185 -> 1834[label="",style="solid", color="burlywood", weight=9];
1834 -> 1189[label="",style="solid", color="burlywood", weight=3];
1835[label="yu101/Zero",fontsize=10,color="white",style="solid",shape="box"];1185 -> 1835[label="",style="solid", color="burlywood", weight=9];
1835 -> 1190[label="",style="solid", color="burlywood", weight=3];
1186[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat Zero yu101 == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="burlywood",shape="box"];1836[label="yu101/Succ yu1010",fontsize=10,color="white",style="solid",shape="box"];1186 -> 1836[label="",style="solid", color="burlywood", weight=9];
1836 -> 1191[label="",style="solid", color="burlywood", weight=3];
1837[label="yu101/Zero",fontsize=10,color="white",style="solid",shape="box"];1186 -> 1837[label="",style="solid", color="burlywood", weight=9];
1837 -> 1192[label="",style="solid", color="burlywood", weight=3];
811[label="span2Zs0 isDigit (Char Zero : yu82) (span2Span1 isDigit yu82 isDigit (Char Zero) yu82 (False && Char Zero <= Char (Succ yu84)))",fontsize=16,color="black",shape="box"];811 -> 821[label="",style="solid", color="black", weight=3];
1096[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat (Succ yu880) (Succ yu890) == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1096 -> 1112[label="",style="solid", color="black", weight=3];
1097[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat (Succ yu880) Zero == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1097 -> 1113[label="",style="solid", color="black", weight=3];
1098[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat Zero (Succ yu890) == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1098 -> 1114[label="",style="solid", color="black", weight=3];
1099[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat Zero Zero == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1099 -> 1115[label="",style="solid", color="black", weight=3];
816[label="span2Ys0 isDigit (Char Zero : yu77) (span2Span1 isDigit yu77 isDigit (Char Zero) yu77 False)",fontsize=16,color="black",shape="box"];816 -> 827[label="",style="solid", color="black", weight=3];
1189[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat (Succ yu1000) (Succ yu1010) == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1189 -> 1195[label="",style="solid", color="black", weight=3];
1190[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat (Succ yu1000) Zero == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1190 -> 1196[label="",style="solid", color="black", weight=3];
1191[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat Zero (Succ yu1010) == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1191 -> 1197[label="",style="solid", color="black", weight=3];
1192[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat Zero Zero == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1192 -> 1198[label="",style="solid", color="black", weight=3];
821[label="span2Zs0 isDigit (Char Zero : yu82) (span2Span1 isDigit yu82 isDigit (Char Zero) yu82 False)",fontsize=16,color="black",shape="box"];821 -> 833[label="",style="solid", color="black", weight=3];
1112 -> 1044[label="",style="dashed", color="red", weight=0];
1112[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat yu880 yu890 == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="magenta"];1112 -> 1127[label="",style="dashed", color="magenta", weight=3];
1112 -> 1128[label="",style="dashed", color="magenta", weight=3];
1113[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (GT == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1113 -> 1129[label="",style="solid", color="black", weight=3];
1114[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (LT == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1114 -> 1130[label="",style="solid", color="black", weight=3];
1115[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (EQ == LT) && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1115 -> 1131[label="",style="solid", color="black", weight=3];
827[label="span2Ys0 isDigit (Char Zero : yu77) (span2Span0 isDigit yu77 isDigit (Char Zero) yu77 otherwise)",fontsize=16,color="black",shape="box"];827 -> 841[label="",style="solid", color="black", weight=3];
1195 -> 1149[label="",style="dashed", color="red", weight=0];
1195[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat yu1000 yu1010 == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="magenta"];1195 -> 1201[label="",style="dashed", color="magenta", weight=3];
1195 -> 1202[label="",style="dashed", color="magenta", weight=3];
1196[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (GT == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1196 -> 1203[label="",style="solid", color="black", weight=3];
1197[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (LT == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1197 -> 1204[label="",style="solid", color="black", weight=3];
1198[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (EQ == LT) && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1198 -> 1205[label="",style="solid", color="black", weight=3];
833[label="span2Zs0 isDigit (Char Zero : yu82) (span2Span0 isDigit yu82 isDigit (Char Zero) yu82 otherwise)",fontsize=16,color="black",shape="box"];833 -> 849[label="",style="solid", color="black", weight=3];
1127[label="yu890",fontsize=16,color="green",shape="box"];1128[label="yu880",fontsize=16,color="green",shape="box"];1129[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not False && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="triangle"];1129 -> 1146[label="",style="solid", color="black", weight=3];
1130[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not True && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1130 -> 1147[label="",style="solid", color="black", weight=3];
1131 -> 1129[label="",style="dashed", color="red", weight=0];
1131[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not False && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="magenta"];841[label="span2Ys0 isDigit (Char Zero : yu77) (span2Span0 isDigit yu77 isDigit (Char Zero) yu77 True)",fontsize=16,color="black",shape="box"];841 -> 857[label="",style="solid", color="black", weight=3];
1201[label="yu1010",fontsize=16,color="green",shape="box"];1202[label="yu1000",fontsize=16,color="green",shape="box"];1203[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not False && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="triangle"];1203 -> 1208[label="",style="solid", color="black", weight=3];
1204[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not True && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1204 -> 1209[label="",style="solid", color="black", weight=3];
1205 -> 1203[label="",style="dashed", color="red", weight=0];
1205[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not False && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="magenta"];849[label="span2Zs0 isDigit (Char Zero : yu82) (span2Span0 isDigit yu82 isDigit (Char Zero) yu82 True)",fontsize=16,color="black",shape="box"];849 -> 865[label="",style="solid", color="black", weight=3];
1146[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (True && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1146 -> 1187[label="",style="solid", color="black", weight=3];
1147[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (False && Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1147 -> 1188[label="",style="solid", color="black", weight=3];
857[label="span2Ys0 isDigit (Char Zero : yu77) ([],Char Zero : yu77)",fontsize=16,color="black",shape="box"];857 -> 874[label="",style="solid", color="black", weight=3];
1208[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (True && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1208 -> 1212[label="",style="solid", color="black", weight=3];
1209[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (False && Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1209 -> 1213[label="",style="solid", color="black", weight=3];
865[label="span2Zs0 isDigit (Char Zero : yu82) ([],Char Zero : yu82)",fontsize=16,color="black",shape="box"];865 -> 883[label="",style="solid", color="black", weight=3];
1187[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (Char (Succ yu86) <= Char (Succ yu90)))",fontsize=16,color="black",shape="box"];1187 -> 1193[label="",style="solid", color="black", weight=3];
1188[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 False)",fontsize=16,color="black",shape="triangle"];1188 -> 1194[label="",style="solid", color="black", weight=3];
874[label="[]",fontsize=16,color="green",shape="box"];1212[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (Char (Succ yu98) <= Char (Succ yu102)))",fontsize=16,color="black",shape="box"];1212 -> 1215[label="",style="solid", color="black", weight=3];
1213[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 False)",fontsize=16,color="black",shape="triangle"];1213 -> 1216[label="",style="solid", color="black", weight=3];
883[label="Char Zero : yu82",fontsize=16,color="green",shape="box"];1193[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (compare (Char (Succ yu86)) (Char (Succ yu90)) /= GT))",fontsize=16,color="black",shape="box"];1193 -> 1199[label="",style="solid", color="black", weight=3];
1194[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span0 isDigit yu87 isDigit (Char (Succ yu86)) yu87 otherwise)",fontsize=16,color="black",shape="box"];1194 -> 1200[label="",style="solid", color="black", weight=3];
1215[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (compare (Char (Succ yu98)) (Char (Succ yu102)) /= GT))",fontsize=16,color="black",shape="box"];1215 -> 1219[label="",style="solid", color="black", weight=3];
1216[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span0 isDigit yu99 isDigit (Char (Succ yu98)) yu99 otherwise)",fontsize=16,color="black",shape="box"];1216 -> 1220[label="",style="solid", color="black", weight=3];
1199[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (compare (Char (Succ yu86)) (Char (Succ yu90)) == GT)))",fontsize=16,color="black",shape="box"];1199 -> 1206[label="",style="solid", color="black", weight=3];
1200[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span0 isDigit yu87 isDigit (Char (Succ yu86)) yu87 True)",fontsize=16,color="black",shape="box"];1200 -> 1207[label="",style="solid", color="black", weight=3];
1219[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (compare (Char (Succ yu98)) (Char (Succ yu102)) == GT)))",fontsize=16,color="black",shape="box"];1219 -> 1225[label="",style="solid", color="black", weight=3];
1220[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span0 isDigit yu99 isDigit (Char (Succ yu98)) yu99 True)",fontsize=16,color="black",shape="box"];1220 -> 1226[label="",style="solid", color="black", weight=3];
1206[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpChar (Char (Succ yu86)) (Char (Succ yu90)) == GT)))",fontsize=16,color="black",shape="box"];1206 -> 1210[label="",style="solid", color="black", weight=3];
1207[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) ([],Char (Succ yu86) : yu87)",fontsize=16,color="black",shape="box"];1207 -> 1211[label="",style="solid", color="black", weight=3];
1225[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpChar (Char (Succ yu98)) (Char (Succ yu102)) == GT)))",fontsize=16,color="black",shape="box"];1225 -> 1231[label="",style="solid", color="black", weight=3];
1226[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) ([],Char (Succ yu98) : yu99)",fontsize=16,color="black",shape="box"];1226 -> 1232[label="",style="solid", color="black", weight=3];
1210 -> 1649[label="",style="dashed", color="red", weight=0];
1210[label="span2Ys0 isDigit (Char (Succ yu86) : yu87) (span2Span1 isDigit yu87 isDigit (Char (Succ yu86)) yu87 (not (primCmpNat (Succ yu86) (Succ yu90) == GT)))",fontsize=16,color="magenta"];1210 -> 1650[label="",style="dashed", color="magenta", weight=3];
1210 -> 1651[label="",style="dashed", color="magenta", weight=3];
1210 -> 1652[label="",style="dashed", color="magenta", weight=3];
1210 -> 1653[label="",style="dashed", color="magenta", weight=3];
1211[label="[]",fontsize=16,color="green",shape="box"];1231 -> 1692[label="",style="dashed", color="red", weight=0];
1231[label="span2Zs0 isDigit (Char (Succ yu98) : yu99) (span2Span1 isDigit yu99 isDigit (Char (Succ yu98)) yu99 (not (primCmpNat (Succ yu98) (Succ yu102) == GT)))",fontsize=16,color="magenta"];1231 -> 1693[label="",style="dashed", color="magenta", weight=3];
1231 -> 1694[label="",style="dashed", color="magenta", weight=3];
1231 -> 1695[label="",style="dashed", color="magenta", weight=3];
1231 -> 1696[label="",style="dashed", color="magenta", weight=3];
1232[label="Char (Succ yu98) : yu99",fontsize=16,color="green",shape="box"];1650[label="yu86",fontsize=16,color="green",shape="box"];1651[label="Succ yu86",fontsize=16,color="green",shape="box"];1652[label="yu87",fontsize=16,color="green",shape="box"];1653[label="Succ yu90",fontsize=16,color="green",shape="box"];1649[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat yu138 yu139 == GT)))",fontsize=16,color="burlywood",shape="triangle"];1844[label="yu138/Succ yu1380",fontsize=10,color="white",style="solid",shape="box"];1649 -> 1844[label="",style="solid", color="burlywood", weight=9];
1844 -> 1690[label="",style="solid", color="burlywood", weight=3];
1845[label="yu138/Zero",fontsize=10,color="white",style="solid",shape="box"];1649 -> 1845[label="",style="solid", color="burlywood", weight=9];
1845 -> 1691[label="",style="solid", color="burlywood", weight=3];
1693[label="yu98",fontsize=16,color="green",shape="box"];1694[label="Succ yu102",fontsize=16,color="green",shape="box"];1695[label="Succ yu98",fontsize=16,color="green",shape="box"];1696[label="yu99",fontsize=16,color="green",shape="box"];1692[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat yu143 yu144 == GT)))",fontsize=16,color="burlywood",shape="triangle"];1846[label="yu143/Succ yu1430",fontsize=10,color="white",style="solid",shape="box"];1692 -> 1846[label="",style="solid", color="burlywood", weight=9];
1846 -> 1733[label="",style="solid", color="burlywood", weight=3];
1847[label="yu143/Zero",fontsize=10,color="white",style="solid",shape="box"];1692 -> 1847[label="",style="solid", color="burlywood", weight=9];
1847 -> 1734[label="",style="solid", color="burlywood", weight=3];
1690[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat (Succ yu1380) yu139 == GT)))",fontsize=16,color="burlywood",shape="box"];1848[label="yu139/Succ yu1390",fontsize=10,color="white",style="solid",shape="box"];1690 -> 1848[label="",style="solid", color="burlywood", weight=9];
1848 -> 1735[label="",style="solid", color="burlywood", weight=3];
1849[label="yu139/Zero",fontsize=10,color="white",style="solid",shape="box"];1690 -> 1849[label="",style="solid", color="burlywood", weight=9];
1849 -> 1736[label="",style="solid", color="burlywood", weight=3];
1691[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat Zero yu139 == GT)))",fontsize=16,color="burlywood",shape="box"];1850[label="yu139/Succ yu1390",fontsize=10,color="white",style="solid",shape="box"];1691 -> 1850[label="",style="solid", color="burlywood", weight=9];
1850 -> 1737[label="",style="solid", color="burlywood", weight=3];
1851[label="yu139/Zero",fontsize=10,color="white",style="solid",shape="box"];1691 -> 1851[label="",style="solid", color="burlywood", weight=9];
1851 -> 1738[label="",style="solid", color="burlywood", weight=3];
1733[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat (Succ yu1430) yu144 == GT)))",fontsize=16,color="burlywood",shape="box"];1852[label="yu144/Succ yu1440",fontsize=10,color="white",style="solid",shape="box"];1733 -> 1852[label="",style="solid", color="burlywood", weight=9];
1852 -> 1739[label="",style="solid", color="burlywood", weight=3];
1853[label="yu144/Zero",fontsize=10,color="white",style="solid",shape="box"];1733 -> 1853[label="",style="solid", color="burlywood", weight=9];
1853 -> 1740[label="",style="solid", color="burlywood", weight=3];
1734[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat Zero yu144 == GT)))",fontsize=16,color="burlywood",shape="box"];1854[label="yu144/Succ yu1440",fontsize=10,color="white",style="solid",shape="box"];1734 -> 1854[label="",style="solid", color="burlywood", weight=9];
1854 -> 1741[label="",style="solid", color="burlywood", weight=3];
1855[label="yu144/Zero",fontsize=10,color="white",style="solid",shape="box"];1734 -> 1855[label="",style="solid", color="burlywood", weight=9];
1855 -> 1742[label="",style="solid", color="burlywood", weight=3];
1735[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat (Succ yu1380) (Succ yu1390) == GT)))",fontsize=16,color="black",shape="box"];1735 -> 1743[label="",style="solid", color="black", weight=3];
1736[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat (Succ yu1380) Zero == GT)))",fontsize=16,color="black",shape="box"];1736 -> 1744[label="",style="solid", color="black", weight=3];
1737[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat Zero (Succ yu1390) == GT)))",fontsize=16,color="black",shape="box"];1737 -> 1745[label="",style="solid", color="black", weight=3];
1738[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat Zero Zero == GT)))",fontsize=16,color="black",shape="box"];1738 -> 1746[label="",style="solid", color="black", weight=3];
1739[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat (Succ yu1430) (Succ yu1440) == GT)))",fontsize=16,color="black",shape="box"];1739 -> 1747[label="",style="solid", color="black", weight=3];
1740[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat (Succ yu1430) Zero == GT)))",fontsize=16,color="black",shape="box"];1740 -> 1748[label="",style="solid", color="black", weight=3];
1741[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat Zero (Succ yu1440) == GT)))",fontsize=16,color="black",shape="box"];1741 -> 1749[label="",style="solid", color="black", weight=3];
1742[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat Zero Zero == GT)))",fontsize=16,color="black",shape="box"];1742 -> 1750[label="",style="solid", color="black", weight=3];
1743 -> 1649[label="",style="dashed", color="red", weight=0];
1743[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (primCmpNat yu1380 yu1390 == GT)))",fontsize=16,color="magenta"];1743 -> 1751[label="",style="dashed", color="magenta", weight=3];
1743 -> 1752[label="",style="dashed", color="magenta", weight=3];
1744[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (GT == GT)))",fontsize=16,color="black",shape="box"];1744 -> 1753[label="",style="solid", color="black", weight=3];
1745[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (LT == GT)))",fontsize=16,color="black",shape="box"];1745 -> 1754[label="",style="solid", color="black", weight=3];
1746[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not (EQ == GT)))",fontsize=16,color="black",shape="box"];1746 -> 1755[label="",style="solid", color="black", weight=3];
1747 -> 1692[label="",style="dashed", color="red", weight=0];
1747[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (primCmpNat yu1430 yu1440 == GT)))",fontsize=16,color="magenta"];1747 -> 1756[label="",style="dashed", color="magenta", weight=3];
1747 -> 1757[label="",style="dashed", color="magenta", weight=3];
1748[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (GT == GT)))",fontsize=16,color="black",shape="box"];1748 -> 1758[label="",style="solid", color="black", weight=3];
1749[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (LT == GT)))",fontsize=16,color="black",shape="box"];1749 -> 1759[label="",style="solid", color="black", weight=3];
1750[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not (EQ == GT)))",fontsize=16,color="black",shape="box"];1750 -> 1760[label="",style="solid", color="black", weight=3];
1751[label="yu1380",fontsize=16,color="green",shape="box"];1752[label="yu1390",fontsize=16,color="green",shape="box"];1753[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not True))",fontsize=16,color="black",shape="box"];1753 -> 1761[label="",style="solid", color="black", weight=3];
1754[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not False))",fontsize=16,color="black",shape="triangle"];1754 -> 1762[label="",style="solid", color="black", weight=3];
1755 -> 1754[label="",style="dashed", color="red", weight=0];
1755[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 (not False))",fontsize=16,color="magenta"];1756[label="yu1440",fontsize=16,color="green",shape="box"];1757[label="yu1430",fontsize=16,color="green",shape="box"];1758[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not True))",fontsize=16,color="black",shape="box"];1758 -> 1763[label="",style="solid", color="black", weight=3];
1759[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not False))",fontsize=16,color="black",shape="triangle"];1759 -> 1764[label="",style="solid", color="black", weight=3];
1760 -> 1759[label="",style="dashed", color="red", weight=0];
1760[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 (not False))",fontsize=16,color="magenta"];1761 -> 1188[label="",style="dashed", color="red", weight=0];
1761[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 False)",fontsize=16,color="magenta"];1761 -> 1765[label="",style="dashed", color="magenta", weight=3];
1761 -> 1766[label="",style="dashed", color="magenta", weight=3];
1762[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (span2Span1 isDigit yu137 isDigit (Char (Succ yu136)) yu137 True)",fontsize=16,color="black",shape="box"];1762 -> 1767[label="",style="solid", color="black", weight=3];
1763 -> 1213[label="",style="dashed", color="red", weight=0];
1763[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 False)",fontsize=16,color="magenta"];1763 -> 1768[label="",style="dashed", color="magenta", weight=3];
1763 -> 1769[label="",style="dashed", color="magenta", weight=3];
1764[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (span2Span1 isDigit yu142 isDigit (Char (Succ yu141)) yu142 True)",fontsize=16,color="black",shape="box"];1764 -> 1770[label="",style="solid", color="black", weight=3];
1765[label="yu137",fontsize=16,color="green",shape="box"];1766[label="yu136",fontsize=16,color="green",shape="box"];1767 -> 1771[label="",style="dashed", color="red", weight=0];
1767[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (Char (Succ yu136) : span2Ys isDigit yu137,span2Zs isDigit yu137)",fontsize=16,color="magenta"];1767 -> 1772[label="",style="dashed", color="magenta", weight=3];
1767 -> 1773[label="",style="dashed", color="magenta", weight=3];
1768[label="yu141",fontsize=16,color="green",shape="box"];1769[label="yu142",fontsize=16,color="green",shape="box"];1770 -> 1774[label="",style="dashed", color="red", weight=0];
1770[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (Char (Succ yu141) : span2Ys isDigit yu142,span2Zs isDigit yu142)",fontsize=16,color="magenta"];1770 -> 1775[label="",style="dashed", color="magenta", weight=3];
1770 -> 1776[label="",style="dashed", color="magenta", weight=3];
1772 -> 728[label="",style="dashed", color="red", weight=0];
1772[label="span2Ys isDigit yu137",fontsize=16,color="magenta"];1772 -> 1777[label="",style="dashed", color="magenta", weight=3];
1773 -> 729[label="",style="dashed", color="red", weight=0];
1773[label="span2Zs isDigit yu137",fontsize=16,color="magenta"];1773 -> 1778[label="",style="dashed", color="magenta", weight=3];
1771[label="span2Ys0 isDigit (Char (Succ yu136) : yu137) (Char (Succ yu136) : yu146,yu145)",fontsize=16,color="black",shape="triangle"];1771 -> 1779[label="",style="solid", color="black", weight=3];
1775 -> 729[label="",style="dashed", color="red", weight=0];
1775[label="span2Zs isDigit yu142",fontsize=16,color="magenta"];1775 -> 1780[label="",style="dashed", color="magenta", weight=3];
1776 -> 728[label="",style="dashed", color="red", weight=0];
1776[label="span2Ys isDigit yu142",fontsize=16,color="magenta"];1776 -> 1781[label="",style="dashed", color="magenta", weight=3];
1774[label="span2Zs0 isDigit (Char (Succ yu141) : yu142) (Char (Succ yu141) : yu148,yu147)",fontsize=16,color="black",shape="triangle"];1774 -> 1782[label="",style="solid", color="black", weight=3];
1777[label="yu137",fontsize=16,color="green",shape="box"];1778[label="yu137",fontsize=16,color="green",shape="box"];1779[label="Char (Succ yu136) : yu146",fontsize=16,color="green",shape="box"];1780[label="yu142",fontsize=16,color="green",shape="box"];1781[label="yu142",fontsize=16,color="green",shape="box"];1782[label="yu147",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs00(yu98, yu99, Succ(yu1000), Zero, yu102) → new_span2Zs01(yu98, yu99, Succ(yu98), Succ(yu102))
new_span2Ys00(yu86, yu87, Succ(yu880), Zero, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))
new_span2Zs01(yu141, yu142, Zero, Zero) → new_span2Zs03(yu141, yu142)
new_span2Ys03(yu136, yu137) → new_span2Zs(yu137)
new_span2Zs01(yu141, yu142, Succ(yu1430), Succ(yu1440)) → new_span2Zs01(yu141, yu142, yu1430, yu1440)
new_span2Ys01(yu136, yu137, Zero, Succ(yu1390)) → new_span2Zs(yu137)
new_span2Zs01(yu141, yu142, Zero, Succ(yu1440)) → new_span2Zs(yu142)
new_span2Zs01(yu141, yu142, Zero, Succ(yu1440)) → new_span2Ys(yu142)
new_span2Zs03(yu141, yu142) → new_span2Ys(yu142)
new_span2Ys01(yu136, yu137, Succ(yu1380), Succ(yu1390)) → new_span2Ys01(yu136, yu137, yu1380, yu1390)
new_span2Ys01(yu136, yu137, Zero, Zero) → new_span2Ys03(yu136, yu137)
new_span2Zs0(Char(Succ(yu8100)), yu82, yu83, yu84) → new_span2Zs00(yu8100, yu82, yu8100, yu83, yu84)
new_span2Ys(:(yu620, yu621)) → new_span2Ys0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Ys00(yu86, yu87, Succ(yu880), Succ(yu890), yu90) → new_span2Ys00(yu86, yu87, yu880, yu890, yu90)
new_span2Zs(:(yu620, yu621)) → new_span2Zs0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
new_span2Ys03(yu136, yu137) → new_span2Ys(yu137)
new_span2Zs02(yu98, yu99, yu102) → new_span2Zs01(yu98, yu99, Succ(yu98), Succ(yu102))
new_span2Zs00(yu98, yu99, Zero, Zero, yu102) → new_span2Zs02(yu98, yu99, yu102)
new_span2Ys00(yu86, yu87, Zero, Zero, yu90) → new_span2Ys02(yu86, yu87, yu90)
new_span2Ys01(yu136, yu137, Zero, Succ(yu1390)) → new_span2Ys(yu137)
new_span2Zs00(yu98, yu99, Succ(yu1000), Succ(yu1010), yu102) → new_span2Zs00(yu98, yu99, yu1000, yu1010, yu102)
new_span2Zs03(yu141, yu142) → new_span2Zs(yu142)
new_span2Ys02(yu86, yu87, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))
new_span2Ys0(Char(Succ(yu7600)), yu77, yu78, yu79) → new_span2Ys00(yu7600, yu77, yu7600, yu78, yu79)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_span2Zs01(yu141, yu142, Succ(yu1430), Succ(yu1440)) → new_span2Zs01(yu141, yu142, yu1430, yu1440)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
new_span2Ys01(yu136, yu137, Succ(yu1380), Succ(yu1390)) → new_span2Ys01(yu136, yu137, yu1380, yu1390)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4
new_span2Zs(:(yu620, yu621)) → new_span2Zs0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
The graph contains the following edges 1 > 1, 1 > 2
new_span2Ys01(yu136, yu137, Zero, Zero) → new_span2Ys03(yu136, yu137)
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Ys(:(yu620, yu621)) → new_span2Ys0(yu620, yu621, Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))))))))))))))))))))))))))))))))))))))))))), Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Succ(Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
The graph contains the following edges 1 > 1, 1 > 2
new_span2Zs01(yu141, yu142, Zero, Zero) → new_span2Zs03(yu141, yu142)
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Zs00(yu98, yu99, Succ(yu1000), Succ(yu1010), yu102) → new_span2Zs00(yu98, yu99, yu1000, yu1010, yu102)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5
new_span2Zs0(Char(Succ(yu8100)), yu82, yu83, yu84) → new_span2Zs00(yu8100, yu82, yu8100, yu83, yu84)
The graph contains the following edges 1 > 1, 2 >= 2, 1 > 3, 3 >= 4, 4 >= 5
new_span2Zs00(yu98, yu99, Succ(yu1000), Zero, yu102) → new_span2Zs01(yu98, yu99, Succ(yu98), Succ(yu102))
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Zs02(yu98, yu99, yu102) → new_span2Zs01(yu98, yu99, Succ(yu98), Succ(yu102))
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Zs00(yu98, yu99, Zero, Zero, yu102) → new_span2Zs02(yu98, yu99, yu102)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 >= 3
new_span2Ys00(yu86, yu87, Zero, Zero, yu90) → new_span2Ys02(yu86, yu87, yu90)
The graph contains the following edges 1 >= 1, 2 >= 2, 5 >= 3
new_span2Ys0(Char(Succ(yu7600)), yu77, yu78, yu79) → new_span2Ys00(yu7600, yu77, yu7600, yu78, yu79)
The graph contains the following edges 1 > 1, 2 >= 2, 1 > 3, 3 >= 4, 4 >= 5
new_span2Ys00(yu86, yu87, Succ(yu880), Succ(yu890), yu90) → new_span2Ys00(yu86, yu87, yu880, yu890, yu90)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5
new_span2Zs03(yu141, yu142) → new_span2Ys(yu142)
The graph contains the following edges 2 >= 1
new_span2Zs03(yu141, yu142) → new_span2Zs(yu142)
The graph contains the following edges 2 >= 1
new_span2Zs01(yu141, yu142, Zero, Succ(yu1440)) → new_span2Ys(yu142)
The graph contains the following edges 2 >= 1
new_span2Zs01(yu141, yu142, Zero, Succ(yu1440)) → new_span2Zs(yu142)
The graph contains the following edges 2 >= 1
new_span2Ys01(yu136, yu137, Zero, Succ(yu1390)) → new_span2Ys(yu137)
The graph contains the following edges 2 >= 1
new_span2Ys01(yu136, yu137, Zero, Succ(yu1390)) → new_span2Zs(yu137)
The graph contains the following edges 2 >= 1
new_span2Ys03(yu136, yu137) → new_span2Ys(yu137)
The graph contains the following edges 2 >= 1
new_span2Ys03(yu136, yu137) → new_span2Zs(yu137)
The graph contains the following edges 2 >= 1
new_span2Ys00(yu86, yu87, Succ(yu880), Zero, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))
The graph contains the following edges 1 >= 1, 2 >= 2
new_span2Ys02(yu86, yu87, yu90) → new_span2Ys01(yu86, yu87, Succ(yu86), Succ(yu90))
The graph contains the following edges 1 >= 1, 2 >= 2

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(yu62, yu63, Succ(yu640), Succ(yu650), yu66) → new_psPs(yu62, yu63, yu640, yu650, yu66)

From the DPs we obtained the following set of size-change graphs:

new_psPs(yu62, yu63, Succ(yu640), Succ(yu650), yu66) → new_psPs(yu62, yu63, yu640, yu650, yu66)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ BR

            ↳ HASKELL

              ↳ COR

                ↳ HASKELL

                  ↳ LetRed

                    ↳ HASKELL

                      ↳ NumRed

                        ↳ HASKELL

                          ↳ Narrow

                            ↳ AND

                              ↳ QDP

                              ↳ QDP

                              ↳ QDP

                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(yu27, yu28, Succ(yu290), Succ(yu300), yu31, yu32) → new_psPs0(yu27, yu28, yu290, yu300, yu31, yu32)

From the DPs we obtained the following set of size-change graphs:

new_psPs0(yu27, yu28, Succ(yu290), Succ(yu300), yu31, yu32) → new_psPs0(yu27, yu28, yu290, yu300, yu31, yu32)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 > 4, 5 >= 5, 6 >= 6

span2Span1	xy xz p wv ww True	= (wv : span2Ys xy xz,span2Zs xy xz)
span2Span1	xy xz p wv ww False	= span2Span0 xy xz p wv ww otherwise